(DML newline () (PROG () (TERPRI)) (/. /-> /.))

(TML)
let printhyp p = map (\x. (printform x; newline())) (hyp(p[]));;



let WEAKFIXRULE th1 th2 =
  let funG = snd (destcomb (rhs (concl th1)))
  and F1 = rhs (concl th2)
  in let f = mkvar (gentok(),typeof F1)
     in let w = "↑f << ↑F1"
        and basis = MIN F1
        in let step = TRANS (APTERM funG (ASSUME w), th2)
           in let concl = INDUCT [funG, f] w (basis,step)
              in SUBS [SYM th1] concl;;

%        ...|- G == FIX funG    ...|- funG F1 << F1
        - - - - - - - - - - - - - - - - - - - - - - -
                      ...|- G << F1
%

let WEAKFIXTAC th ((w,ss,fml):goal) =
   let funG = snd (destcomb (rhs (concl th)))
   and F1 = rhs w
   in ([mkinequiv (mkcomb (funG, F1), F1), ss, fml],
       WEAKFIXRULE th o hd);;

% takes a goal of the form ("G << FF", ss, fml)
                   and a thm |- G == FIX funG

  and produces a subgoal of form ("funG FF << FF",ss,fml)
%




let RECINDRULE th =
  let funG = fst (destcomb (rhs (concl th)))
  and G    = lhs (concl th)
    in let f = mkvar (gentok(), typeof G)
      in let w = "↑f << ↑G"
        and basis = MIN G
          in let step = TRANS(APTERM funG (ASSUME w), SYM th)
            in INDUCT[funG,f] w (basis,step) ;;

%            ...|- G == funG G
            - - - - - - - - - -
             ...|- FIX funG << G
%


let RECINDTAC ((w,ss,fml):goal) =
  let funG = snd(destcomb(lhs w))
  and    G = rhs w
    in ([mkequiv(G,mkcomb(funG,G)), ss, fml],
        RECINDRULE o hd) ;;

% takes a goal of the form ("FIX funG << G", ss, fml)
  
  and produces a subgoal of form ("G == funG G, ss, fml)
%


letrec destcons2 firstpart l = null l => fail |
                     null (tl l) => (firstpart, hd l) |
                     destcons2 (firstpart @ [hd l]) (tl l);;

%     [e1; ... ;en]         to        [e1; ... ;en-1],en        %


letrec SPECL th varlist =
   let conc = concl th
     in isquant conc =>
                      let var = fst (destquant conc)
                        in SPECL (SPEC var th) (var . varlist)
                     | (varlist,th);;


% |- !xn ... !x1.w  , []    to   [x1 ... xn], |- w        %



letrec GENL l th = null l => th | GENL (tl l) (GEN (hd l) th);;

% [xn ... x1], |- w        to    |- !x1 ... !xn.w         %


let EXTL th =
  isquant (concl th) =>
    let varlist,th' = SPECL th nil
       in let restofvars,lastvar = destcons2 nil varlist
         in GENL restofvars (EXT (GEN lastvar th'))
                     | th;;

%         |- !x1 ... !xn. P xn ... x1 =< Q xn ... x1
          - - - - - - - - - - - - - - - - - - - - - -
          |- !x2 ... !xn. P xn ... x2 =< Q xn ... x1
%
        


letrec takeapart (l , w) =
  isquant w => let c,d = destquant w in
               takeapart (c.l, d) |
  isequiv w => (l,(true,destequiv w)) |
  isinequiv w => (l,(false,destinequiv w)) | fail;;

letrec mkquantl l w =
  null l => w | mkquantl (tl l) (mkquant ((hd l),w));;

let APPLYTAC2 ((w,ss,fml):goal) =
  let varlist,b,F,G = takeapart (nil,w)
  in let x = mkvar (gentok(), fst(destfuntype(typeof F)))
     in let w' =  b => (mkquant (x, (mkquantl varlist
                          (mkequiv (mkcomb (F,x),mkcomb(G,x)))))) |
                       (mkquant (x, (mkquantl varlist
                          (mkinequiv (mkcomb (F,x),mkcomb(G,x))))))
         in ([w' ,ss,fml] , (EXTL o hd) );;

% takes a goal of the form  "F =< G" or "!x.F x =< G x"
  where "F:*->**" or "F:*->**->***" resp.
  and produces a subgoal of the form "!x.F x =< G x" or
  "!y.!x.F x y =< G x y" resp.
%



letrec destquantl (l,w) = isquant w => let c,d = destquant w
                                     in destquantl ((c.l), d) |
                                     (l,w) ;;

letrec ITSPEC l th = null l => th | ITSPEC (tl l) (SPEC (hd l) th);;

letrec reverse l1 l2 = null l1 => l2 | reverse (tl l1) ((hd l1).l2) ;;


let USEIHTAC ((w,ss,fml):goal) =
   letref FML = fml
   in ((let IH = ASSUME (hd FML)
      in let boundvars,rest = destquantl (nil, (hd FML))
         in let matchlist = fst (termmatch ([]:term list,
                           []:type list) (lhs rest) (lhs w))
            in let speclist = reverse
                              ((map (fst o (\e. revassoc e matchlist)))
                                   boundvars) nil
                in let IH' = ITSPEC speclist IH
                   in aconvform (w, (concl IH')) =>
                      ([w, (ssadd IH ss), fml],
                       hd) | fail)
                     ! FML := tl FML)
                     ? failwith `USEIHTAC`;;


let ANTIBETATAC ((w,ss,fml):goal) =
  let t2,t1 = destequiv w in
    let g = mkvar(gentok(),typeof t2) in
      let newt1=substinterm[(g,t2)] t1 in
        let t3 = mkcomb(mkabs(g,newt1),t2) in
          ([mkequiv(t2,t3),ss,fml],
           (SUBS[(BETACONV t3)]) o hd);;

%goal is  t2==t1 with t1 contains t2.
 In the subgoal t1 is replaced by
 (\g:type-of-t2. t1[g/t2])(t2)
%


let GREUTAC ((w,ss,fml):goal) =
  ([w,itlist ssadd (map ASSUME fml) ss,fml],hd);;

let UNWINDTAC th ((w,ss,fml):goal) =
    let tha = FIX th
    in let thb = TRANS (tha, BETACONV (rhs (concl tha)))
       in let F,unwound = destequiv (concl thb)
       in ([(substinform [unwound,F] w),ss,fml],
           (SUBS [SYM thb] o hd));;


let UNWINDOCCSTAC nlist th ((w,ss,fml):goal) =
   let tha = FIX th
   in let thb = TRANS (tha, BETACONV (rhs (concl tha)))
      in let F, unwound = destequiv (concl thb)
      in ([(substoccsinform [unwound,nlist,F] w),ss,fml],
          (SUBS [SYM thb] o hd));;



letrec dequantify th = 
  let wl,w = destthm th in
    isquant w => (let x,w' = destquant w in 
                    let x' = variant(x, formlfrees(w' .wl)) in
                      dequantify(SPEC x' th)
                 )
               | th ;;

%buggy: wrong format  for the subst...




let ANTIBETAOCCSTAC nl t1:term t2 ((w,ss,fml):goal) =
  let g = mkvar (gentok(),typeof t2)
    in let newt1 = substinterm (g,t2,t1)
       in let t3 = mkcomb (mkabs (g,newt1),t2)
          in ([substoccsinform (nl,t3,t1,w),ss,fml],
              (SUBSOCCS nl (SYM (BETACONV t3))) o hd);;

%
%goal contains some instance of t1 which contains an instance of
 t2.   In the subgoal, that instance of t1 is replaced by
  "(\g:t2.t1[g/t2]) (t2)"
%